$\forall$$T$:Type, $P$:($T$$\rightarrow$prop\{i:l\}), $x$:$T$, $L$:($T$ List).
\\[0ex]l\_all(cons($x$; $L$); $T$; $y$.$P$($y$)) $\Leftarrow\!\Rightarrow$ ($P$($x$) $\wedge$ l\_all($L$; $T$; $y$.$P$($y$)))